use crate::disvec::DisVec;
use std::fs::File;
use std::io::Read;

pub type LitMem = Vec<DisVec>;

pub fn read_ws(cur: &mut &[u8]) {
  while let Some(&c) = cur.first() {
    match c {
      b'\t'..=b'\r' | b' ' => *cur = &cur[1..],
      _ => break,
    }
  }
}

pub fn read_nl(cur: &mut &[u8]) {
  while let Some(&c) = cur.first() {
    if c == b'\n' {
      *cur = &cur[1..];
      break;
    } else {
      *cur = &cur[1..];
    }
  }
}

pub fn read_num(cur: &mut &[u8]) -> i32 {
  read_ws(cur);
  let mut sgn = 1;
  if let Some(&b'-') = cur.first() {
    sgn = -1;
    *cur = &cur[1..];
  }
  let mut num = 0;
  while let Some(&c) = cur.first() {
    match c {
      b'0'..=b'9' => {
        num = num * 10 + (c - b'0') as i32;
        *cur = &cur[1..];
      }
      _ => break,
    }
  }
  num * sgn
}

pub fn parse(filename: &str, lit_mem: &mut LitMem, var_num: &mut usize, cla_num: &mut usize) {
  let mut file = File::open(filename).expect("Unable to open file");
  let mut data = Vec::new();
  file.read_to_end(&mut data).expect("Unable to read file");

  let mut cur = &data[..];
  let mut buf = DisVec::new();

  while !cur.is_empty() {
    read_ws(&mut cur);
    match cur.first() {
      Some(&b'%') => break,
      Some(&b'c') => {
        read_nl(&mut cur);
      }
      Some(&b'p') => {
        if cur.len() >= 5 && &cur[0..5] == b"p cnf" {
          cur = &cur[5..];
          *var_num = read_num(&mut cur) as usize;
          *cla_num = read_num(&mut cur) as usize;
        } else {
          panic!("Invalid format: expected 'p cnf <var> <clauses>'");
        }
      }
      Some(_) => {
        let lit = read_num(&mut cur);
        if lit == 0 {
          lit_mem.push(buf.clone());
          buf = DisVec::new();
        } else {
          buf.set(lit);
        }
      }
      None => break,
    }
  }
}
